$\forall$$A$:Type, ${\it eq}$:EqDecider($A$), $B$:($A$$\rightarrow$Type), $P$:($A$$\rightarrow\mathbb{B}$), $f$:fpf($A$; $x$.$B$($x$)), $x$:$A$, $v$:$B$($x$).
\\[0ex]($<$$x$, $v$$>$ $\in$ fpf{-}vals(${\it eq}$; $P$; $f$))
\\[0ex]$\Leftarrow\!\Rightarrow$ guard(((($\uparrow$fpf{-}dom(${\it eq}$; $x$; $f$)) $\wedge$ ($\uparrow$($P$($x$)))) $\wedge$ ($v$ = fpf{-}ap($f$; ${\it eq}$; $x$))))